%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%   Springer-Verlag compatible format. After reducing to 13.5x   %%%%
%%%%   20cm the fontsize is exactly 10pt.	-Rob van Glabbeek   %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\documentstyle[12pt]{article}		 % Fontsize 12 point	       %
\textwidth		16.2 cm		 % A4 width is 21cm	       %
\textheight		24   cm		 % A4 height is 29.7cm	       %
\oddsidemargin		-0.14cm	 	 % +1 inch = 2.4cm	       %
\evensidemargin		-0.14cm		 % +1 inch = 2.4cm	       %
\topmargin		-0.14cm		 % +1 inch = 2.4cm	       %
\headheight		 0   cm		 % foot with pagenumber 1.06cm %
\headsep		 0   cm		 % thus 2.24cm left at bottom. %
\parindent		 0   cm		 % Paragraphs not indented ... %
\parskip	6pt plus 2pt minus 1 pt	 % but some space between them %
\unitlength		 1   mm		 % This is used in pictures    %
\thinlines                        	 % alternative: Thicklines     %
\renewcommand{\baselinestretch}{1.1}     % More space between the lines%
\frenchspacing                           % No larger distance after a .%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%   On American paper the right margin is 6 mm larger, whereas   %%%%
%%%%   the bottom margin is 17.6 mm shorter. 	-Rob van Glabbeek   %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newlength{\shiftside}			 \newlength{\shifttop}
\setlength{\shiftside}{3mm}		 \setlength{\shifttop}{-8.8mm}
\typeout{On what kind of paper are you going to print this?}
\typein[\paper]{Enter 0 for A4 or 1 for American paper.}
\addtolength\oddsidemargin{\paper\shiftside}
\addtolength\evensidemargin{\paper\shiftside}
\addtolength\topmargin{\paper\shifttop}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%   The following implements a layout and numbering convention   %%%%
%%%%   chosen by Ursula Goltz.  All theorem-like environments are   %%%%
%%%%   indented and in roman. Numbering of theorems, propositions   %%%%
%%%%   etc. happens separately and by section.   All environments   %%%%
%%%%   have two  arguments:  a label for future reference,  and a   %%%%
%%%%   header for basic assumptions like "Let S be a set".   -Rob   %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{defi}{Definition}[section]
\newtheorem{theo}{Theorem}[section]
\newtheorem{prop}{Proposition}[section]
\newtheorem{lem}{Lemma}[section]
\newtheorem{cor}{Corollary}[section]
\newtheorem{exam}{Example}[section]

\newenvironment{Definition}[2]{\begin{defi} \rm \label{def-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{defi}}

\newenvironment{Theorem}[2]{\begin{theo} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{theo}}

\newenvironment{Proposition}[2]{\begin{prop} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{prop}}

\newenvironment{Lemma}[2]{\begin{lem} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{lem}}

\newenvironment{Corollary}[2]{\begin{cor} \rm \label{#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{cor}}

\newenvironment{Example}[2]{\begin{exam} \rm \label{ex-#1} \mbox{#2}
\begin{itemize} \vspace{-.7em} \item[]}{\end{itemize}\end{exam}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\IN}{\mbox{\rm I\hspace{-0.8mm}N}}
\newcommand{\IE}{\mbox{\rm I\negthinspace E}}
\newcommand{\qed}{\hfill $\Box$ \par \vskip 0.25cm}
\newcommand{\conf}{{\it Conf\/}}
\newcommand{\reff}{{\it ref\/}}
\newcommand{\Act}{{\it Act\/}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\mbox{\ }\vspace{3em}

\begin{center}
{\LARGE\bf Interleaving Semantics \\
and Action Refinement with Atomic Choice\\}
\end{center}

\vskip 1cm

\begin{center}
{\large Ingo Czaja}\\
{\small Gesellschaft f\"ur Mathematik und Datenverarbeitung\\
Postfach 1316, D-5205 Sankt Augustin, Germany}
\vspace{2ex}

{\large Rob J. van Glabbeek}\\
{\small Computer Science Department, Stanford University\\
Stanford, CA 94305, USA\\
\tt rvg@cs.stanford.edu}
\vspace{2ex}

{\large Ursula Goltz}\\
{\small Gesellschaft f\"ur Mathematik und Datenverarbeitung\\
Postfach 1316, D-5205 Sankt Augustin, Germany\\
\tt goltz@gmdzi.gmd.de}
\end{center}

\vskip 1.5cm

We investigate how to restrict the concept of {\it action refinement} such that
established interleaving equivalences for concurrent systems are preserved under
these restricted refinements. We show that {\it interleaving bisimulation} is
preserved under refinement if we do not allow to refine action occurrences
deciding choices and action occurrences involved in autoconcurrency.
On the other hand, {\it interleaving trace equivalence} is
still not preserved under these restricted refinements.

\vspace{2em minus .6em}
{\bf Keywords\ } Concurrency, action refinement, atomicity, flow event
structures, semantic equivalences, interleaving vs. partial orders,
bisimulation.

\vspace{1em minus .3em}
{\bf Notes\ } This paper appeared as Arbeitspapiere der GMD 594, Sankt
Augustin 1991.
The work presented here has partly been carried out
within the Esprit Basic Research Action 3148 (DEMON) and the
Sonderforschungsbereich 182 of the University of Erlangen-N\"urnberg.

\section{Introduction}

For the design of concurrent systems, it can be useful to consider a
hierarchy of representations, which allows refinement of unstructured
entities on a more abstract design level by complex structures on a
lower level. One approach which is being investigated is {\it action
refinement} where the entities being refined are the actions
which a system may perform. A single action in an abstract view may
correspond to a process consisting of many actions in a more concrete representation.
Action refinement is being investigated in process algebras [Aceto, AH, NEL] and in
semantic models of concurrent systems [GG a/b/c, Vogler a/b, BDKP, Devillers, DD a/b,
BGV].

Action refinement can be modelled as an operator, taking a system description $P$ on a
given level of abstraction as well as a refinement function \reff\ associating processes
with actions, and yielding a system description $\reff (P)$ on a lower level, obtained
by replacing action occurrences by occurrences of the associated processes. It differs
from many other operators that are considered for concurrent systems in that applying it
on a representation of a system does not yield a representation of a different system,
but a different representation of the same system.

An important question being considered is the following: Which
equivalence notions for concurrent systems are {\it preserved under
refinement\/}? Taking two system representations, $P,Q$, which are equivalent for some
equivalence notion $\sim$, we would expect that $\reff (P) \sim \reff (Q)$ for any
refinement function $\reff $. This expectation indicates a big difference between
action refinement and many other approaches for moving to a lower level of abstraction,
in which adding more information about the precise implementation of systems makes it
more likely that systems turn out to be different that were indistinguishable
on the higher level of abstraction. Our expectation is based on the idea that in the original
system representations $P$ and $Q$ it is not known how the actions will be implemented.
However, it is decided that different occurrences of the same action will be
implemented in the same way, so that any difference between $P$ and $Q$ that could arise
after refinement is already visible in the abstract representations, namely through
the use of different action names for corresponding events.

The preservation question has been addressed in
the papers mentioned above. The usual approach to this problem is: Take some
well-established equivalence notion. If it is not preserved under refinement, try to
find the coarsest equivalence notion contained in it which has this property (see e.g.
[Vogler a/b]).

What has not been considered so far is the following question. Given a
well-established equivalence notion which is not preserved under
refinement, is there a way of restricting either the allowed refinements or the class
of system representations under consideration such that preservation of this equivalence
in the restricted setting is obtained? This question is addressed in the present paper
for two of the most basic equivalences.

We consider system descriptions in which the basic building blocks are the actions
which may occur in a system. In our approach an action can be any activity which is
considered as a conceptual entity on a chosen level of abstraction. Now we distinguish
{\it atomic} actions that cannot be refined, and compound ones that can. One can
think of atomic actions as being instantaneous and of compound actions as durational.
Many approaches to concurrency in which actions are not supposed to be refined, in
particular the {\it interleaving} approaches, in which parallelism is equated with
arbitrary interleaving of action occurrences, can be thought of as dealing exclusively
with the subclass of system representations were all actions in a system are atomic. On
the other hand the action refinement approaches cited above take the possibility into
account that {\it any} action can be refined. In this paper we look at systems in which
some actions are atomic, and others can be refined. In particular we consider systems in
which all action occurrences deciding choices, as well as all actions that can occur
concurrently with themselves are atomic. These restrictions turn out to be sufficient to
apply action refinement in certain interleaving semantics, while preserving semantic
equivalence. Although the distinction between atomic and compound actions may be useful
for motivating this research, technically one may just as well drop this distinction and
restrict the class of allowed refinement functions to a class of what
we call {\it safe} refinements. Those refinements
 do not refine action occurrences deciding choices and actions involved in autoconcurrency.

It turns out that the {\it branching structure} (i.e. the relative order of action
occurrences and choices between different courses of action) of concurrent systems plays
a r\^{o}le in our results. We show that {\it interleaving bisimulation}, where the
branching structure between alternative executions is taken into account, is preserved
under safe refinements. On the other hand, we show that {\it interleaving trace
equivalence} (where the branching structure is fully neglected) is still not preserved
under these restricted refinements. To investigate safe refinements for equivalence notions between
these two extremes in the linear time -- branching time spectrum has to be left for future research.

\section{Basic Notions}

We consider systems which are capable of performing actions from a
given set {\it Act} of action names. By an action we understand here any
activity which is considered as an conceptual entity on a chosen level
of abstraction. We will not distinguish external and internal actions;
we do not consider abstraction by hiding of actions in this paper.

We will sometimes give process algebra terms for examples to make them
easier to understand: $+$ will denote choice (as in CCS), $\mid$ will denote
parallel composition (without communication), $a,b,...\in Act$ denote
actions, and ; denotes a general sequential composition operator (like
the one of ACP). The semicolon will sometimes be omitted and we use the
usual precedence rule that ; binds stronger than the other operators.
However this notation is only used for intuition; formally our results
are established for {\it event structures}.

We will describe a concurrent system by a set of events where each
event corresponds  to an occurrence of some action. Therefore, events are
labelled by action names.

The simplest form of event structures has been introduced in [NPW]
and is usually referred to as {\it prime event structures} with binary
conflicts. A labelled prime event structure is a tuple $(E,<,\#,l)$ where
$E$ is the set of events, $<~ \subseteq  E \times E$ is an (irreflexive)
partial order (the {\it causality relation}), $~\#~ \subseteq E \times E$ is
the so-called {\it conflict relation}, and $l : E \rightarrow Act$ specifies
the labelling of events by action names.
As usual, we require $<$ to satisfy the {\it axiom of finite causes}\/; that is,
any event may have only finitely many predecessors. Furthermore, $\#$ is
required to be irreflexive and symmetric and to respect the axiom of conflict
heredity: $\forall d,e,f \in E : d~\#~e \wedge d < f \Longrightarrow e~\#~f.$

A prime event structure represents a concurrent system in the following way:
action names $a \in Act$ represent actions the system may perform, an event
$e \in E$ labelled with $a$ represents an occurrence of $a$ during a possible
run of the system, $d < e$ means that $d$ is a prerequisite for $e$ and
$d~\#~e$ means that $d$ and $e$ cannot happen both in the same run.

The behaviour of a prime event structure is described by explaining which
subsets of events constitute possible runs of the represented system. These
subsets are called {\it configurations}. They have to be conflict-free and they
must be left-closed with respect to $<$ (all prerequisites for any event
occurring in the run must also occur).

As shown in [GG a], prime event structures are well suited to define a notion
of action refinement, as long as actions are not refined by behaviours
containing conflicts.

But as a consequence of the axioms explained above, it is cumbersome to define
a more general notion of refinement directly for prime event structures.
Whenever a given event occurs, it has to be ``enabled" by a unique set of events
that is independent of the particular run of the system, namely by all its
predecessors according to the causality relation. However, when refining
$a$ by $a_1 + a_2$ in $a\,;b$, $b$ should occur alternatively caused by $a_1$ or
by $a_2$. In prime event structures, this may only be modelled by duplicating the
$b$-event, leading to complicated definitions and proofs. Hence more expressive event
structure representations are being used for refinement. {\it Free event structures}\/
as defined in [DD a] seem to be weakest extension of prime event structures to allow
refinements with conflicts in a straightforward way. However, difficulties with the
interpretation of the notion of causality in this model lead in [DD b] to a restriction
such that prime event structures are no longer a subclass. In [GG a, GG b], {\it flow
event structures} [BC] have been used which are also a convenient model for CCS. This
is the model we have chosen here as well, in order to establish our results also for
refinements with conflicts.

We will now introduce the main concepts of flow event structures following
closely [Boudol].

\pagebreak
\begin{Definition}{flow-es} {  }
A {\it (labelled) flow event structure (over an
alphabet \Act)} is a 4-tuple \\ ${\cal E} = (E,\prec,\#,l)$, where
\begin{itemize}
\item $ E $ is a set of {\it events},
\item $ \prec~\subseteq E \times E $ is an irreflexive relation, the
{\it flow relation},
\item $ \# \subseteq E \times E $ is a symmetric relation, the
{\it conflict relation},
\item $l: E \longrightarrow $\Act\ is the {\it labelling function}.
\end{itemize}
\end{Definition}

Let \IE\ denote the domain of flow event structures labelled over {\it Act}.
The components of ${\cal E} \in$ \IE\ will be denoted by
$E_{\cal E}, \prec_{\cal E}, \#_{\cal E}$ and $l_{\cal E}$. The index ${\cal E}$
will be omitted if clear from the context.
% ${\cal E}$ is {\it conflict-free} if $\# = \emptyset$.\\
% For $X \subseteq E_{\cal E}$, ${\cal E} \lceil X =
% (X, \prec_{\cal E}\hspace{-2mm}\lceil X, \#_{\cal E} \lceil X, l_{\cal E} \lceil X)$
% is the {\it restriction of ${\cal E}$ to $X$}.

Two flow event structures ${\cal E}$ and ${\cal F}$ are {\it isomorphic}
(${\cal E} \cong {\cal F}$) iff there exists a bijection between their
sets of events preserving $\prec,\#$ and labelling.
Often, we will not distinguish isomorphic event structures; the names of events
are not important for us.

The interpretation of the conflict and the flow relation is formalised by
defining  configurations of flow event structures. Configurations must be
conflict free; in particular, self-conflicting events will never occur in any
configuration. $d \prec e$ will mean that $d$ is a {\it possible immediate cause}
for $e$. For an event to occur it is necessary that a {\it complete}
non-conflicting set of its causes has occurred. Here a set of causes is complete
if for any cause which is not contained there is a conflicting event which is
contained. Finally, no cycles with respect to causal dependence may occur.

We will only consider finite configurations here. As usual, we assume
that in a finite period of time only finitely many actions may be
performed. Now the requirement says that we only consider runs which
are executable in a finite period of time. This is no restriction since
the infinite configurations which are usually considered are completely
determined by the finite ones (see e.g. [Boudol]).

\begin{Definition}{configurations} {Let ${\cal E} \in $ \IE.}
\begin{itemize} 
\item [(i)] $X \subseteq E$ is {\it left-closed up to conflicts} iff
$\forall d,e \in E$: if $e \in X, d \prec e$ and $d \not\in X$ then there
exists an $f \in X$ with $f \prec e$ and $d~\#~f$.

$X \subseteq E$ is {\it conflict-free} iff $\#_{\cal E} \lceil
X = \emptyset$. 
\item [(ii)]
$X \subseteq E$ is a {\it (finite) configuration} of ${\cal E}$ iff
$X$ is finite, left-closed up to conflicts and conflict-free and does
not contain a
causality cycle: $<_X~ := (\prec \cap(X \times X))^+$ is irreflexive.
$\conf ({\cal E})$ denotes the set of all (finite) configurations of
${\cal E}$.

\item[(iii)]
A configuration $X \in \conf ({\cal E})$ is called {\it maximal}
iff $X \subseteq Y \in \conf ({\cal E})$ implies $X = Y$.
It is {\it complete} iff
$\forall d \in E : d \not\in X \Rightarrow \exists e \in X$ with $d~\#~e$.
\end{itemize} 
\end{Definition}

The relation $<_X$ expresses causal dependence in the configuration $X$. 
Note that prime event structures are special flow event structures
defining $d \prec e$ iff $d < e$. In prime event structures, the
requirement of left-closedness up to conflicts for configurations
reduces to left-closedness: $\forall d,e \in E :$ if $e \in X \wedge d <
e$ then $d \in X$; furthermore, in each configuration $X$, the relation
$<_X$ coincides with $<$.
However in prime event structures every maximal configuration is complete,
whereas in flow event structures this need not be the case (although every
complete configuration must be maximal). In [GG c] the difference between
complete and maximal configurations is used to model deadlock behaviour:
complete configurations indicate successful termination, whereas incomplete
maximal configurations model deadlocks.

The following observations may offer some additional motivation for the 
definition of configurations above.

\begin{Definition}{enabling}{Let ${\cal E} \in$ \IE, $X \in \conf ({\cal
E})$.}
\begin{itemize}
\item[(i)]
$X$ {\it enables} $e \in E$ iff $e\notin X$ and $X \cup \{e\} \in \conf ({\cal
E})$. \item[(ii)]
A subset $Y \subseteq X$ is a {\em
prefix} of $X$ iff $\forall d \in X,\ e \in Y:\ d <_X e \Rightarrow d
\in Y$ (i.e. $Y$ is left-closed in $X$ w.r.t. $<_X$).
\end{itemize}
\end{Definition}

\begin{Proposition}{enabling}{Let ${\cal E} \in$ \IE, $X \in \conf ({\cal
E})$.} \begin{itemize}
\item[(i)] $X$ enables $e$ iff $e \not\in X, \neg(\exists d \in X$ with $d \#
e)$ and $\forall d \prec e$ we have $d \in X \vee \exists f \in X$ with $f \prec
e$ and $d\# f$. \item[(ii)] $X$ can be written as $X = \{e_1, \dots , e_n\}$ such
that for $k < n: \{e_1, \dots ,e_k\} $ enables $e_{k+1}$. \item[(iii)] For $Y
\subseteq X$, $Y \in \conf ({\cal E})$ iff $Y$ is a prefix of $X$.
\end{itemize} \end{Proposition}

{\bf Proof\ \ } See [Boudol]. \qed
 
We now define transition relations between configurations, describing which
event or which action may occur in a configuration and which configuration
may then be obtained.


\begin{Definition}{transitions}{Let ${\cal E} \in $ \IE.}

$ X \buildrel {e} \over \longrightarrow_{\cal E} X' $ iff
$X$ enables $e$ and $X'=X\cup\{e\}$.\\
$ X \buildrel {a} \over \longrightarrow_{\cal E} X' $ iff
$ X \buildrel {e} \over \longrightarrow_{\cal E} X'$ and $ l(e) = a\in\Act$.
\end{Definition}

The index ${\cal E}$ is omitted if clear from the context.

Next we introduce a relation $co_X$ expressing when two events are
{\it concurrent} (independent) within a configuration $X$, as well as a global
relation $co$, expressing {\it possible concurrency}, and show that the
relations correspond. Furthermore we define when there is a {\it choice}
between two events.

\begin{Definition}{choice}
{Let ${\cal E} \in$ \IE.}
\begin{itemize}
\item[(i)]
For $X \in \conf ({\cal E})$, let $co_X \subseteq X \times X$ be defined by \\
$d~co_X~e $ iff $\neg(d <_X e \vee e <_X d) $ .

\item[(ii)] $co \subseteq E \times E$ is defined by \\
$d~co~e$ iff $\exists X \in \conf ({\cal E})$, $X$ enables both $d$ and $e$
and $X \cup \{d,e\} \in \conf ({\cal E})$.

\item[(iii)] $ch \subseteq E \times E$ is defined by \\
$d~ch~e$ iff $\exists X \in \conf ({\cal E})$, $X$ enables both $d$ and $e$
and $X \cup \{d,e\} \not\in \conf ({\cal E})$.
\end{itemize}
\end{Definition}


\begin{Proposition}{choice}
{Let ${\cal E} \in$ \IE, $d ,e \in E$.}
\begin{itemize}
\item[(i)]
$d~co~e~\Leftrightarrow ~\exists X \in \conf ({\cal E})$ with $d~co_X~e$.
\item[(ii)]
$d~ch~e~\Rightarrow~d~\#~e$.
\end{itemize}
\end{Proposition}

{\bf Proof\ \ } \\
(i): \\
``$\Rightarrow$":
Let $d~co~ e$. Then there exists $X\in\conf({\cal E})$ with $d,e$ both enabled
by $X$. \\ Let $Y:=X\cup \{d,e\}$. We show that $d~co_Y~ e$.\\
Assume $d<_Y e$. Then $X \cup \{e\}$ would not be a prefix of $Y$, hence $X \cup
\{e\}$ would not be a configuration and $e$ not enabled by $X$.
Thus $\neg (d<_Y e)$ and by symmetry $\neg (e<_Y d)$.

``$\Leftarrow$":
Let $X \in \conf ({\cal E})$ with $d~co_X~e$.
Let $X' = X - \{f \in X \mid d <_X f \vee e <_X f\}$.\\
$d,e \in X'$, since $d,e \in X$ and $d$ and $e$ are not in $<_X$-relation. \\
Moreover $d$ and $e$ are maximal in $X'$ w.r.t. $<_X$.\\
Let $X_1 := X'-\{d\}$, $X_2 := X'-\{e\}$, $X'' := X' - \{d,e\}$.\\
Then $X',X_1,X_2,X'' \in \conf ({\cal E})$ with proposition \ref{enabling}(iii)
and $d ~co~e$.

(ii):\\
Suppose $d~ch~e$, but $\neg(d~\#~e)$. 
We show that for each configuration $X$ enabling $d$ and $e$, also $X' := X \cup
\{d,e\}$ is a configuration.\\
Let $X \in \conf ({\cal E})$, with 
$X \buildrel {d} \over \longrightarrow X_1$ and
$X \buildrel {e} \over \longrightarrow X_2$.
Let $X' := X \cup \{d,e\}$.

$X'$ is finite, since $X \in \conf ({\cal E})$.

$X'$ is conflict-free, since $X_1, X_2 \in \conf ({\cal E})$ and
$\neg(d~\#~e)$.

$X'$ is left-closed up to conflicts:\\
Suppose $f \in X'$, $g \in E-X'$ and $g \prec f$. Then $f \in X_i$ for $i=1$ or
$i=2$ and $g \not\in X_i$, so $\exists h \in X_i \subseteq X'$ with $h \prec f$
and $g \# h$, since $X_i \in \conf ({\cal E})$.

$X'$ contains no cycles w.r.t. $\prec$:\\
Suppose $X'$ contains a  causality cycle. Since $X_2 \in \conf ({\cal E})$ this
cycle must contain $d$. However, we will show that there is no $c \in X'$ with
$d \prec c$. Since $X,X_1 \in \conf ({\cal E})$, $X$ must be a prefix of $X_1$
by proposition \ref{enabling}(iii), implying that $d$ is maximal in $X_1$.
Thus the only candidate for $c$ is $e$. So suppose $d \prec e$. Since
$d \not\in X_2$ and $e 
\in X_2 \in \conf ({\cal E})$ there must be an $f \in X_2 \subseteq X'$ with $f
\prec e$ and $d \# f$, contradicting the conflict-freeness of $X'$.

Thus $X' \in \conf ({\cal E})$.
\qed

For prime event structures, the choice relation coincides with the
non-inherited conflicts.

\begin{Definition}{immediate-conflict}{Let ${\cal E}\in$ \IE\ be a prime
event structure.}
$\#^1\subseteq E\times E$ ({\it immediate conflict}) is defined by\\ 
$d~\#^1 e$ iff $d~\#~e$, $f < d \Rightarrow \neg(f~\#~e) $ and $f < e
\Rightarrow \neg(f~\#~d) $. \end{Definition}

\begin{Proposition}{immediate-conflict}{Let ${\cal E}\in$ \IE\ be a prime
event structure, $d,e\in E$.} Then $d~ch~e ~\Leftrightarrow ~ d~\#^1 e$.
\end{Proposition}

{\bf Proof\ \ }  \\
``$\Rightarrow$": Let $d~ch~e$. Then there exists $X\in \conf ({\cal E})$
enabling both $d$ and $e$. \\ $d\#e$ by proposition \ref{choice}.\\
Assume there is an $f$ with $f<d$. Then $f\in X$, since $X\cup \{d\}$ is
left-closed. Since $f\in X\cup \{e\}\in \conf ({\cal E})$, we have $\neg (f\#e)$.
\\Similarly $f < e \Rightarrow \neg(f~\#~d) $.

``$\Leftarrow$":
Let $d~\#^1 e$. Let $X:=\{f\in E ~|  \ f<d \vee f<e\}$.\\
Since $d~\#~e$ it cannot be the case that $d<e$ or $e<d$ by the axiom of
conflict heredity and the irreflexivity of $\#$. Thus $d,e\notin X$.\\
Let $X_1=X\cup \{d\}$ and $X_2:=X\cup \{e\}$.\\
Since $d~\#~e$ we have $X\cup \{d,e\} \notin \conf ({\cal E})$, so it suffices to
prove that $X,X_1$ and $X_2$ are configurations.

$X,X_1$ and $X_2$ are finite (axiom of finite causes).\\
$X,X_1$ and $X_2$ are left-closed (transitivity of $<$).\\
$X,X_1$ and $X_2$ are conflict-free:\\
It suffices to prove that $X_1$ is conflict-free, since this implies that $X$
is conflict-free, and the conflict-freeness of $X_2$ follows by symmetry.\\
Suppose $d',e'\in X_1$ and $d'~\#~e'$. We may assume $d'\leq d$ and $e'<e$,
since the cases that $d'$ and $e'$ are both predecessors of $d$ or of $e$ are
excluded by the axiom of conflict heredity and the irreflexivity of $\#$.
But then $d~\#~e'$ by conflict heredity, violating the definition of $\#^1$.  
\qed

Note that for prime event structures the conflict relation is
fully determined by the immediate conflicts, and hence by the choice relation.
On the other hand, in flow event structures the choice relation does not
determine the conflict relation. Moreover, the part of the conflict relation
that is not determined by the choice relation influences the set of
configurations (as well as the deadlock behaviour [GG c]).

\newpage
\begin{Example}{choice}{ }
Consider the following two flow event structures, where the labelling is the
identity. Here and later we represent the flow relation by arrows of the form
\begin{picture}(11,2)
\put(0,1){\line  (1,0){11}}
\put(0,1){\vector(1,0){ 6}}
\end{picture}.

\begin{picture}(149,37)(-20,5)
\put( 5,36){\makebox(0,0)[b]{${\cal E} =$}}
\put(20,36){\makebox(0,0)[b]{$a$}}
\put(30,36){\makebox(0,0)[b]{$\#$}}
\put(40,36){\makebox(0,0)[b]{$b$}}
\put(30,28.5){\makebox(0,0)[b]{$\#$}}
\put(40,21){\makebox(0,0)[b]{$c$}}
\put(30, 7){\makebox(0,0)[b]{$d$}}
\put(22,35){\line  (4,-3){ 6}}
\put(32,27.5){\line  (4,-3){ 6}}
\put(21,35){\line  (1,-3){ 8.33}}
\put(21,35){\vector(1,-3){ 4.5}}
\put(40,35){\line  (0,-1){11}}
\put(40,35){\vector(0,-1){ 6}}
\put(39,20){\line  (-3,-4){ 7.5}}
\put(39,20){\vector(-3,-4){ 4}}

\put(65,36){\makebox(0,0)[b]{${\cal F} =$}}
\put(80,36){\makebox(0,0)[b]{$a$}}
\put(90,36){\makebox(0,0)[b]{$\#$}}
\put(100,36){\makebox(0,0)[b]{$b$}}
\put(100,21){\makebox(0,0)[b]{$c$}}
\put(90, 7){\makebox(0,0)[b]{$d$}}
\put(81,35){\line  (1,-3){ 8.33}}
\put(81,35){\vector(1,-3){ 4.5}}
\put(100,35){\line  (0,-1){11}}
\put(100,35){\vector(0,-1){ 6}}
\put(99,20){\line  (-3,-4){ 7.5}}
\put(99,20){\vector(-3,-4){ 4}}
\end{picture}

In both event structures the events $a$ and $c$ are in {\it semantic conflict}, in the
sense that they cannot occur in the same configuration. However, in ${\cal F}$ they are
not in {\it syntactic conflict\/}: $\neg (a ~\#_{\cal F}~ c)$. \\ We have $E_{\cal
E}=E_{\cal F}$, $\prec _{\cal E}~=~\prec _{\cal F}$ and  $l _{\cal E}=l _{\cal F}$.
Moreover the choice relations of ${\cal E}$ and ${\cal F}$ agree: only $a~ch~b$.
Nevertheless ${\cal E}$ has a configuration $\{a,d\}$ which ${\cal F}$ has not.
\end{Example}   

Refinement of actions in flow event
structures may now be defined as follows. We assume a refinement function $\reff
: Act \longrightarrow$ \IE$ - \{O\} $ (where $O$ denotes the empty flow event
structure) and replace each event labelled by $a$ by a disjoint copy of $\reff
(a)$. The conflict and causality structure will be inherited. Refinements in which some
actions are replaced by the empty process can drastically change the behaviour of
concurrent systems and can not be explained by a change in the level of abstraction at
which these systems are regarded [GG a]. Therefore they are not considered here.

\begin{Definition}{refinement}{  }
\begin{itemize}
\item [(i)] A function $\reff  :
Act \longrightarrow $\IE$ - \{O\}$ is called a
{\it refinement function} .
\item[(ii)] Let ${\cal E} \in $ \IE\ and let $\reff $ be a refinement function.
\\ Then the {\it refinement of ${\cal E}$ by $\reff $}, $\reff ({\cal E}) $,
is the flow event structure defined by
\begin{itemize}
\item [$-$] $E_{\reff ({\cal E})} = \{(e,e') \mid e \in E_{\cal E},
   e' \in E_{\reff (l_{\cal E}(e))} \} $,
\item [$-$] $(d,d') \prec_{\reff ({\cal E})} (e,e') $ iff $d \prec_{\cal E} e$ or
   ($d = e \wedge d' \prec_{\reff (l_{\cal E}(d))} e') $,
\item [$-$] $(d,d')~\#_{\reff ({\cal E})}~(e,e')$ iff $d~\#_{\cal E}~e$ or
   ($d = e \wedge d'~\#_{\reff (l_{\cal E}(d))}~e') $,
\item [$-$] $l_{\reff ({\cal E})}(e,e') = l_{\reff (l_{\cal E}(e))}(e')$ .
\end{itemize}
\end{itemize}
\end{Definition}

The following examples illustrate that the usual interleaving equivalences
are not preserved under this refinement operation.

The event structures we consider in examples from now on will always be prime; hence we
will only draw immediate conflicts and omit arcs for the elements of the flow relation
obtainable by transitivity.

\newpage
\begin{Example}{interleaving-choice}{  }
Consider the event structures ${\cal E}$ and ${\cal F}$ below, corresponding to $a|b$
and $ab+ba$.

\begin{picture}(149,25)(-15,3)
\put(15,21){\makebox(0,0)[b]{${\cal E} =$}}
\put(30,21){\makebox(0,0)[b]{$a$}}
\put(40,21){\makebox(0,0)[b]{$b$}}

\put(65,21){\makebox(0,0)[b]{${\cal F} =$}}
\put(80,21){\makebox(0,0)[b]{$a$}}
\put(80, 6){\makebox(0,0)[b]{$b$}}
\put(90,21){\makebox(0,0)[b]{$\#$}}
\put(100,21){\makebox(0,0)[b]{$b$}}
\put(100, 6){\makebox(0,0)[b]{$a$}}
\put(80,20){\line  (0,-1){10}}
\put(80,20){\vector(0,-1){ 5}}
\put(100,20){\line  (0,-1){10}}
\put(100,20){\vector(0,-1){ 5}}
\end{picture}

${\cal E}$ and ${\cal F}$ are indistinguishable in any kind of
interleaving semantics. We refine action $a$ by $a_1 a_2$, i.e. $\reff (a) =$
\begin{picture}(22,2)
\put(4,0){\makebox(0,0)[br]{$a_1$}}
\put(17,0){\makebox(0,0)[bl]{$a_2$,}}
\put(5,1){\line  (1,0){11}}
\put(5,1){\vector(1,0){ 6}}
\end{picture} and then have

\begin{picture}(149,40)(-15,3)
\put(15,36){\makebox(0,0)[b]{$\reff ({\cal E}) =$}}
\put(30,36){\makebox(0,0)[b]{$a_1$}}
\put(40,36){\makebox(0,0)[b]{$b$}}
\put(30,35){\line  (0,-1){10}}
\put(30,35){\vector(0,-1){ 5}}
\put(30,21){\makebox(0,0)[b]{$a_2$}}
\put(45,36){\makebox(0,0)[b]{,}}

\put(65,36){\makebox(0,0)[b]{$\reff ({\cal F}) =$}}
\put(80,36){\makebox(0,0)[b]{$a_1$}}
\put(80,21){\makebox(0,0)[b]{$a_2$}}
\put(80, 6){\makebox(0,0)[b]{$b$}}
\put(90,36){\makebox(0,0)[b]{$\#$}}
\put(100,36){\makebox(0,0)[b]{$b$}}
\put(100,21){\makebox(0,0)[b]{$a_1$}}
\put(100, 6){\makebox(0,0)[b]{$a_2$}}
\put(80,20){\line  (0,-1){10}}
\put(80,20){\vector(0,-1){ 5}}
\put(100,20){\line  (0,-1){10}}
\put(100,20){\vector(0,-1){ 5}}
\put(80,35){\line  (0,-1){10}}
\put(80,35){\vector(0,-1){ 5}}
\put(100,35){\line  (0,-1){10}}
\put(100,35){\vector(0,-1){ 5}}
\put(105,36){\makebox(0,0)[b]{.}}
\end{picture}

$\reff ({\cal E})$ and $\reff ({\cal F})$ are not interleaving equivalent,
since $a_1 b\, a_2 $ is a possible execution of $\reff ({\cal E})$ but not of
$\reff ({\cal F})$.
\end{Example}

\begin{Example}{interleaving-autoconcurrency}{  }
Consider the event structures ${\cal E}$ and ${\cal F}$ below, corresponding to $a|a$
and $aa$.

\begin{picture}(149,24)(-15,4)
\put(15,21){\makebox(0,0)[b]{${\cal E} =$}}
\put(30,21){\makebox(0,0)[b]{$a$}}
\put(40,21){\makebox(0,0)[b]{$a$}}

\put(65,21){\makebox(0,0)[b]{${\cal F} =$}}
\put(80,21){\makebox(0,0)[b]{$a$}}
\put(80, 7){\makebox(0,0)[b]{$a$}}
\put(80,20){\line  (0,-1){10}}
\put(80,20){\vector(0,-1){ 5}}
\end{picture}

${\cal E}$ and ${\cal F}$ are indistinguishable in common interleaving
semantics. We refine $a$ by $a_1 a_2$ and then have

\begin{picture}(149,46)(-15,6)
\put(15,45){\makebox(0,0)[b]{$\reff ({\cal E}) =$}}
\put(30,45){\makebox(0,0)[b]{$a_1$}}
\put(40,45){\makebox(0,0)[b]{$a_1$}}
\put(30,33){\makebox(0,0)[b]{$a_2$}}
\put(40,33){\makebox(0,0)[b]{$a_2$}}
\put(40,44){\line  (0,-1){8}}
\put(40,44){\vector(0,-1){4.5}}
\put(30,44){\line  (0,-1){8}}
\put(30,44){\vector(0,-1){4.5}}
\put(45,45){\makebox(0,0)[b]{,}}

\put(65,45){\makebox(0,0)[b]{$\reff ({\cal F}) =$}}
\put(80,45){\makebox(0,0)[b]{$a_1$}}
\put(80,33){\makebox(0,0)[b]{$a_2$}}
\put(80,21){\makebox(0,0)[b]{$a_1$}}
\put(80, 9){\makebox(0,0)[b]{$a_2$}}
\put(80,44){\line  (0,-1){8}}
\put(80,44){\vector(0,-1){4.5}}
\put(80,32){\line  (0,-1){8}}
\put(80,32){\vector(0,-1){4.5}}
\put(80,20){\line  (0,-1){8}}
\put(80,20){\vector(0,-1){4.5}}
\put(85,45){\makebox(0,0)[b]{.}}
\end{picture}

Now $\reff ({\cal E})$ and $\reff ({\cal F})$ are not interleaving equivalent,
since only in $\reff ({\cal E})$ it is possible to start with two occurrences of $a_1$.
\end{Example}

We observe that in example \ref{ex-interleaving-choice} an event of ${\cal F}$ is
refined which decides a choice. In example \ref{ex-interleaving-autoconcurrency}, an
action is refined which may occur concurrently with itself. Hence we have identified two classes of
events which will definitely cause problems for interleaving semantics if they are refined.
We will now call actions labelling such events
{\it critical\/} (with respect to a particular event structure ${\cal E}$) and consider
the subclass of flow event structures where all critical actions are atomic, in the
sense that they cannot really be refined. We could restrict the allowed refinement
functions such that atomic actions may only be `refined' by themselves. However, our
refinement theorem will hold even in a slightly more general setting. First of all we
may allow {\it renaming} of atomic actions, obtained by refining them by
conflict-free event structures containing exactly one event, as well as {\it
restriction} of certain (atomic) actions, obtained by refining them by
event structures consisting of one self-conflicting event. In this way the relabelling
and restriction operators of CCS can still be understood as instances of the refinement
operator. Moreover we allow {\it generalised renamings}, replacing (atomic) actions by
(possibly infinite) choices $a_1+a_2+...$\,. The crucial restriction is that the
execution of any event of a refined atomic action $a$ leads to its immediate
termination, thereby preserving atomicity for these actions. Formally this is ensured if
and only if every non-empty configuration of $\reff (a)$ is complete. This can be
obtained by requiring that all events of $\reff (a)$ are mutually in conflict. 

\begin{Definition}{critical}{Let ${\cal
E} \in~$\IE.} \begin{itemize} \item[(i)] An action $a \in \Act $ is {\it critical} in
${\cal E}$ iff \\ $\exists d, e \in E$ with $d~ch~e$ and $l(d) = a$ \quad or \\ $\exists
d, e \in E$, $d \neq e$ with $d~co~e$ and $l(d) = l(e) = a$.

$Crit_{\cal E} := \{a \in Act \mid a $~is critical in $ {\cal E} \}$
is the set of all critical actions in ${\cal E}$.
\item[(ii)]
A refinement function $\reff $ is called {\it safe} w.r.t. ${\cal E}$ iff \\
$\forall a \in~ Crit_{\cal E} ~ \forall d,e \in E_{\reff (a)},~ d \neq e :~ d
\#_{\reff(a)} e$. \end{itemize}
\end{Definition}

\begin{Proposition}{critical}{Let ${\cal
E} \in~$\IE, $a\in Crit_{\cal E}$, and $\reff$ a safe refinement w.r.t. ${\cal E}.$} 
Then every non-empty configuration of $\reff (a)$ is complete.
\end{Proposition}
{\bf Proof\ \ }  Trivial. \qed

In flow event structures it may be difficult to find out which actions are critical and
should therefore be atomic. A safe strategy is to avoid autoconcurrency altogether and
make every event which is in conflict with another event atomic. The result of this strategy
depends on the particular flow event structure representation of a system by
the choice of a syntactic conflict relation $~\#~$ (recall that semantic and syntactic conflict do not
coincide for flow event structures). The most liberal possibilities for refinement are
obtained by choosing a minimal conflict relation to model the intended behaviour.

\newpage
\section{Interleaving trace semantics}

We now investigate whether interleaving equivalences are preserved by safe
refinements. We start by considering the simplest notion, the usual
{\it interleaving trace equivalence} where the possible sequences of actions are
compared.

\begin{Definition}{trace}{  }
$w = a_1 \dots a_n \in \Act^*$
is a {\it (sequential) trace} of ${\cal E} \in $ \IE\  iff \\
$\exists X_0, \dots , X_n \in \conf ({\cal E}): X_0 = \emptyset$ and
$X_{i-1} \buildrel {a_i} \over \longrightarrow X_i$ , $i = 1, \dots, n$.

$SeqTraces({\cal E})$
denotes the set of all sequential traces of ${\cal E}$.

${\cal E}, {\cal F} \in $ \IE~ are called {\it interleaving trace equivalent}
(${\cal E} \approx_{it} {\cal F}$) iff \\
$SeqTraces({\cal E}) = SeqTraces({\cal F})$.
\end{Definition}

The following example shows that this equivalence is not preserved
by safe refinements.

\begin{Example}{trace}{  }
Consider the event structures ${\cal E}$ and ${\cal F}$ below, corresponding to $a(b|c)$
and $abc+acb$.

\begin{picture}(149,40)(-10,11)
\put(15,44){\makebox(0,0)[b]{${\cal E} =$}}
\put(40,44){\makebox(0,0)[b]{$a$}}
\put(26,29){\makebox(0,0)[b]{$b$}}
\put(54,29){\makebox(0,0)[b]{$c$}}
\put(38,43){\line  (-1,-1){10}}
\put(38,43){\vector(-1,-1){5}}
\put(42,43){\line  (1,-1){10}}
\put(42,43){\vector(1,-1){5}}

\put( 75,44){\makebox(0,0)[b]{${\cal F} =$}}
\put( 90,44){\makebox(0,0)[b]{$a$}}
\put(110,44){\makebox(0,0)[b]{$a$}}
\put(100,44){\makebox(0,0)[b]{$\#$}}
\put( 90,29){\makebox(0,0)[b]{$b$}}
\put(110,29){\makebox(0,0)[b]{$c$}}
\put( 90,14){\makebox(0,0)[b]{$c$}}
\put(110,14){\makebox(0,0)[b]{$b$}}
\put( 90,43){\line  (0,-1){10}}
\put( 90,43){\vector(0,-1){5}}
\put( 90,28){\line  (0,-1){10}}
\put( 90,28){\vector(0,-1){5}}
\put(110,43){\line  (0,-1){10}}
\put(110,43){\vector(0,-1){5}}
\put(110,28){\line  (0,-1){10}}
\put(110,28){\vector(0,-1){5}}
\end{picture}

${\cal E} \approx_{it} {\cal F}$, since the only traces for both event structures
are $abc$ and $acb$ (and the prefixes).
Action $b$ is not critical.
We refine $b$ by $b_1 b_2$. 

\begin{picture}(149,57)(-10,4)
\put(15,53){\makebox(0,0)[b]{$\reff ({\cal E}) =$}}
\put(40,53){\makebox(0,0)[b]{$a$}}
\put(26,38){\makebox(0,0)[b]{$b_1$}}
\put(26,23){\makebox(0,0)[b]{$b_2$}}
\put(54,38){\makebox(0,0)[b]{$c$}}
\put(38,52){\line  (-1,-1){10}}
\put(38,52){\vector(-1,-1){5}}
\put(42,52){\line  (1,-1){10}}
\put(42,52){\vector(1,-1){5}}
\put(26,37){\line  (0,-1){10}}
\put(26,37){\vector(0,-1){5}}

\put( 75,53){\makebox(0,0)[b]{$\reff ({\cal F}) =$}}
\put( 90,53){\makebox(0,0)[b]{$a$}}
\put(110,53){\makebox(0,0)[b]{$a$}}
\put(100,53){\makebox(0,0)[b]{$\#$}}
\put( 90,38){\makebox(0,0)[b]{$b_1$}}
\put( 90,23){\makebox(0,0)[b]{$b_2$}}
\put(110,38){\makebox(0,0)[b]{$c$}}
\put( 90, 8){\makebox(0,0)[b]{$c$}}
\put(110,23){\makebox(0,0)[b]{$b_1$}}
\put(110, 8){\makebox(0,0)[b]{$b_2$}}
\put( 90,52){\line  (0,-1){10}}
\put( 90,52){\vector(0,-1){5}}
\put( 90,37){\line  (0,-1){10}}
\put( 90,37){\vector(0,-1){5}}
\put( 90,22){\line  (0,-1){10}}
\put( 90,22){\vector(0,-1){5}}
\put(110,52){\line  (0,-1){10}}
\put(110,52){\vector(0,-1){5}}
\put(110,37){\line  (0,-1){10}}
\put(110,37){\vector(0,-1){5}}
\put(110,22){\line  (0,-1){10}}
\put(110,22){\vector(0,-1){5}}
\end{picture}

We have $\reff ({\cal E})~\not\approx_{it}~\reff ({\cal F})$, since
$ab_1c \in SeqTraces(\reff ({\cal E}))$, \\
but $ab_1c \not\in SeqTraces(\reff ({\cal F}))$.
\end{Example}

One can now ask if it is possible to strengthen the requirement of
safe refinements, say into {\it trace-safe} refinements, by requiring
more actions to be atomic, in such a way that interleaving trace
equivalence is preserved under trace-safe refinements. Requiring all
actions that can occur concurrently with another action to be atomic
would work, but this constraint is very restrictive. It seems not easy
to find a less restrictive one.

\section{Interleaving bisimulation semantics}

In this section we will show that interleaving bisimulation equivalence
[Park, Milner] is preserved under safe refinements.

\begin{Definition}{bisimulation}
{Let ${\cal E}, {\cal F} \in $ \IE.}
A relation $R \subseteq \conf ({\cal E})
\times \conf ({\cal F})$ is called an {\it interleaving bisimulation between}
${\cal E}$ {\it and} ${\cal F}$ iff
$(\emptyset, \emptyset) \in R$, and if $(X,Y) \in R$ then
\begin{itemize}
\item $X \buildrel a \over \longrightarrow X' \Rightarrow
\exists Y' $ with $Y \buildrel a \over \longrightarrow Y'$ and
$(X',Y') \in R$,
\item $Y \buildrel a \over \longrightarrow Y' \Rightarrow
\exists X' $ with $X \buildrel a \over \longrightarrow X'$ and
$(X',Y') \in R$.
\end{itemize}
${\cal E}$ and ${\cal F}$ are {\it interleaving bisimulation equivalent}
(${\cal E} \approx_{ib} {\cal F}$) iff there exists an interleaving
bisimulation between ${\cal E}$ and ${\cal F}$ .
\end{Definition}

In [GG a] it has been shown that the configurations of a refined event
structure may be deduced compositionally from the configurations of the
original event structure and those of the refinements of actions.
We will use this result and the following lemmas in the proof of the
refinement theorem.


\begin{Definition}{compositionality}
{Let ${\cal E} \in$ \IE, let $\reff $ be a refinement function.}
\begin{itemize} \item[(i)]
We call $\tilde X$ a {\it refinement of a configuration} $X \in \conf ({\cal
E})$ {\it by} $\reff $ iff
\begin{itemize}
\item [$-$] $ \tilde X = \bigcup\limits_{e \in X} (\{e\} \times X_e )$
where $ \forall e \in X : X_e \in \conf (\reff (l_{\cal E}(e))) - \{ \emptyset \} $,
\item [$-$] $ busy(\tilde X) \subseteq max(X)$ where
\begin{itemize}
\item $max(X)$ denotes the set of all maximal events in $X$ w.r.t. $<_X$,
\item $busy(\tilde X) := X - compl(\tilde X)$ and
\item $compl(\tilde X) := \{e \in X \mid X_e~$is a complete configuration$ \}$.
\end{itemize}
\end{itemize}
\item[(ii)] $\reff (X)$ denotes the set of refinements of $X \in \conf ({\cal E})$ by
\reff \\ and for $S \subseteq \conf ({\cal E})$, $\reff (S)= \displaystyle \bigcup_{X
\in S} \reff (X)$.
\end{itemize}
\end{Definition}


Clearly, if $\tilde X \in \reff (X)$ then $X = pr(\tilde X) :=
\{ e \in E_{\cal E} \mid \exists e' \in E_{\reff (l(e))} : (e,e') \in \tilde X \}$
and we have $compl(\tilde X) \subseteq pr(\tilde X)$,
$pr(\tilde X) - max(pr(\tilde X)) \subseteq compl(\tilde X)$.

\begin{Proposition}{compositionality}{[GG a] Let ${\cal E} \in $ \IE, let $\reff $ be a
refinement function.} Then $\conf (\reff ({\cal E})) = \reff (\conf ({\cal E}))$.
\end{Proposition}

\begin{Lemma}{1}
{Let $ {\cal E} \in~ $\IE,
$\reff $ a refinement function and $ \tilde X \in \conf (\reff ({\cal E}))$.}
If $compl(\tilde X) \subseteq Y \subseteq pr(\tilde X)$
then $ Y \in \conf ({\cal E})$.
\end{Lemma}

{\bf Proof\ \ }
Immediate from proposition \ref{enabling}(iii), since $pr(\tilde X) -
max(pr(\tilde X)) \subseteq Y \subseteq pr(\tilde X)$. \qed

With lemma \ref{1} we have in particular $compl(\tilde X) \in \conf ({\cal E}) $.

\begin{Lemma}{2}
{Let $ {\cal E} \in $ \IE,
$ X \in \conf ({\cal E}) $ and $ a \not\in Crit_{\cal E}$.}
$ X \buildrel a \over \longrightarrow X_1 ,~
X \buildrel a \over \longrightarrow X_2 \Rightarrow X_1 = X_2 $.
\end{Lemma}

{\bf Proof\ \ } Immediate from the definitions. \qed

\begin{Lemma}{3}
{Let $ {\cal E} \in $ \IE, $\reff$ a safe refinement function w.r.t. ${\cal E}$
and $ \tilde X \in \conf (\reff ({\cal E})) $.} 
If $ e \in pr(\tilde X) - compl(\tilde X)$ then $l_{\cal E}(e) \not\in Crit_{\cal E}$.
\end{Lemma}

{\bf Proof\ \ } With proposition \ref{compositionality} we have $X_e \in \conf (\reff
(l_{\cal E}(e))) - \{ \emptyset \}$. \\If $l_{\cal E}(e) \in Crit_{\cal E}$ than $X_e$ is
complete by proposition \ref{critical}. \\However, since $ e \in  pr(\tilde X) -
compl(\tilde X) $, $X_e$ is not complete.
\qed

\begin{Lemma}{4}
{Let $ {\cal E} \in $ \IE, $\reff$ a safe refinement function w.r.t. ${\cal E}$
and $ \tilde X \in \conf (\reff ({\cal E})) $.} 
If $compl(\tilde X) \cup \{e\} \in \conf ({\cal E})$
then $ pr(\tilde X) \cup \{e\} \in \conf ({\cal E})$.
\end{Lemma}

{\bf Proof\ \ }
W.l.o.g. we assume that $e \not\in pr(\tilde X)$.\\
With proposition \ref{enabling}(i) we prove that $pr(\tilde X)$ enables $e$.

Suppose $\exists d \in pr(\tilde X)$ with $d\#e$. Since $compl(\tilde X) \cup \{e\} $ is
conflict-free, it follows that $d \in pr(\tilde X) - compl(\tilde X)$.
Thus $compl(\tilde X)$ enables $d$ (with lemma \ref{1}) as well as $e$, so $d~ch~e$.
However, with lemma \ref{3} we have $l(d) \not\in Crit_{\cal E}$, contradicting $d~ch~e$.

Now suppose $d \prec e$ and $d \notin pr(\tilde X) \supseteq compl(\tilde X)$.
Since $compl(\tilde X) \cup \{e\} \in \conf ({\cal E})$ there is an $f \in compl(\tilde
X) \subseteq pr(\tilde X)$ with $f \prec e $ and $d\#f$.
\qed

With these lemmas we can prove the theorem.

\begin{Theorem}{refinement}
{Let $ {\cal E}, {\cal F} \in $ \IE, let
$ \reff  $ be a safe refinement function w.r.t. ${\cal E}$ and ${\cal F}$.}
Then$\quad {\cal E} \approx_{ib} {\cal F} \quad
\Rightarrow \quad \reff ({\cal E}) \approx_{ib} \reff ({\cal F}) $.
\end{Theorem}

{\bf Proof\ \ } Let $ {R} $ be a bisimulation between $ {\cal E} $
and $ {\cal F} $. \\
Let $ \tilde R = \{(\tilde X, \tilde Y) \in
\conf (\reff ({\cal E})) \times \conf (\reff ({\cal F})) \mid $ \\
\phantom{Let $ \tilde R = \{$}
$ (compl(\tilde X), compl(\tilde Y)) \in R , $ \\
\phantom{Let $ \tilde R = \{$}
there exist bijections $ f: pr(\tilde X) \longrightarrow pr(\tilde Y)$
with $ l_{\cal F}(f (e)) = l_{\cal E}(e) $ \\
\phantom{Let $ \tilde R = \{$}
and $ \tilde f: \tilde X \longrightarrow \tilde Y $
with $ \tilde f (e,e') = (f(e),e') \} $

We show that $ \tilde R $ is a bisimulation
between $\reff ({\cal E}) $ and $ \reff ({\cal F}) $.

i.\phantom{i} Obviously $ (\emptyset,\emptyset) \in \tilde R$.

ii. Let $ (\tilde X,\tilde Y) \in \tilde R$. Then
$ (compl(\tilde X), compl(\tilde Y)) \in R$ and there are bijections
$ f$ and $\tilde f$ as required in the definition of $\tilde R$.
We have to show the bisimulation properties.
It suffices to check one of them, the other follows by symmetry.

Let $\tilde X \buildrel a \over \longrightarrow \tilde X'$.
Let $\tilde X' - \tilde X = \{(e^{\mbox{\scriptsize o}},e^*)\}$, $l_{\cal E} (e^{\mbox{\scriptsize o}}) = b$.
Then $l_{\reff ({\cal E})} ((e^{\mbox{\scriptsize o}},e^*)) = l_{\reff (b)} (e^*) = a$. \\
Now we have to show :
$ \exists \tilde Y' \in \conf (\reff ({\cal F})) $ with $
\tilde Y \buildrel a \over \longrightarrow \tilde Y' $ and $
(\tilde X',\tilde Y') \in  \tilde R$.\\
For the construction of $ \tilde Y' $, we distinguish two cases.\\[2.5em]
{\bf 1. $pr(\tilde X') = pr(\tilde X) $.}

In this case we can use the bijection $f$ to define $\tilde Y'$, since
its domain is not affected by adding the new event.

Let $ \tilde Y' :=
\{ (f(e),e') \mid (e,e') \in \tilde X' \} $. \\
With $\tilde Y = \{ (f(e),e') \mid (e,e') \in \tilde X\}$ we have
$ \tilde Y' = \tilde Y \cup \{(f(e^{\mbox{\scriptsize o}}),e^*)\} $.

First we show that $\tilde Y'$ is a configuration with $\tilde Y
\buildrel a \over \longrightarrow \tilde Y'$.\\
Then we define the new functions $f'$ and $\tilde f'$ and check their properties.\\
Finally we prove $(compl(\tilde X'),compl(\tilde Y')) \in R$.

With proposition \ref{compositionality} we show $\tilde Y' \in \conf (\reff ({\cal F}))
$:
\begin{itemize} \vspace{-.7em}
\item [$-$] $pr(\tilde Y') = f(pr(\tilde X')) = f(pr(\tilde X)) =
pr(\tilde Y) \in \conf ({\cal F})$, since $ \tilde Y \in \conf (\reff ({\cal F}))$;
\item [$-$] $\forall d \in  pr(\tilde Y') $:
$  Y_d' =  X_{f^{-1}(d)}' \in \conf (\reff (l_{\cal E}(f^{-1}(d)))) -
\{\emptyset \} = \conf (\reff (l_{\cal F}(d))) - \{\emptyset \}$,
since $ \tilde X' \in \conf (\reff ({\cal E}))$;
\item [$-$] $busy(\tilde Y') = pr(\tilde Y') - compl(\tilde Y') \subseteq pr(\tilde Y) -
compl(\tilde Y) \subseteq max(pr(\tilde Y)) = max(pr(\tilde Y'))$, since $pr(\tilde Y)
= pr(\tilde Y')$ and $compl(\tilde Y) \subseteq compl(\tilde Y')$.
\end{itemize} \vspace{-.7em}
Thus $\tilde Y'$ is a configuration of $ \reff ({\cal F})$.\\
Since $l_{\reff ({\cal F})} ((f(e^{\mbox{\scriptsize o}}),e^*)) = l_{\reff (b)} (e^*) = a$ we have $ \tilde Y
\buildrel a \over \longrightarrow \tilde Y'$.

Let $ f' := f $ and $ \tilde f' := \tilde f \cup \{((e^{\mbox{\scriptsize o}},e^*),(f(e^{\mbox{\scriptsize o}}),e^*))\}$.
The new function $\tilde f'$ is bijective, since the events $(e^{\mbox{\scriptsize o}},e^*)$ and
$(f(e^{\mbox{\scriptsize o}}),e^*)$ do not occur in the domain and the range of $\tilde f$, respectively.
By construction $f'$ and $\tilde f'$ have the required properties.

In order to establish $ (\tilde X',\tilde Y') \in \tilde R $ we still have to show
$ (compl(\tilde X'), compl(\tilde Y')) \in R$.\\
Again we have two cases:
\begin{description}
\item[1.1. $ compl(\tilde X') = compl(\tilde X) $.] {\ }\\
Using the properties of $\tilde f'$, $compl(\tilde Y') = f'(compl(\tilde X')) =
f(compl(\tilde X)) = compl(\tilde Y)$, hence $(compl(\tilde X'),compl(\tilde Y')) \in  R
$.
\item [1.2. $ compl(\tilde X') \neq compl(\tilde X) $.] {\ }\\
Then $compl(\tilde X') = compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\}$ and
$ compl(\tilde X) \buildrel b \over \longrightarrow compl(\tilde X')$.

Since $(compl(\tilde X),compl(\tilde Y)) \in R$ there is a $ Y' \in \conf ({\cal F}) $
with $compl(\tilde Y)~\buildrel b \over \longrightarrow~Y'$ and
$(compl(\tilde X'), Y') \in R$.

Using the properties of $\tilde f'$, $compl(\tilde Y') = f'(compl(\tilde X')) =
f(compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\}) = compl(\tilde Y) \cup \{f(e^{\mbox{\scriptsize o}})\}$, hence
$compl(\tilde Y) \buildrel b \over \longrightarrow compl(\tilde Y')$.

Since $e^{\mbox{\scriptsize o}} \in compl(\tilde X') \subseteq pr(\tilde X') = pr(\tilde X)$,
it follows that $e^{\mbox{\scriptsize o}} \in pr(\tilde X) - compl(\tilde X)$ and with lemma \ref{3}
$b = l_{\cal E} (e^{\mbox{\scriptsize o}}) \not\in Crit_{\cal E}$. Hence $Y' = compl(\tilde Y')$ with lemma
\ref{2}.

Thus $(compl(\tilde X'), compl(\tilde Y')) \in R$, which had to be proved.
\end{description}
\vspace{1em}
%---------------------------------Beweis 2.------------------------------------
{\bf 2. $pr(\tilde X') \neq pr(\tilde X)$.}

The proof of the second case is similar to that of the first case. However
the construction of $\tilde Y'$ is more complicated since we cannot just use
the function $f$. We need to describe the events by which $f$ is extended.

$pr(\tilde X') = pr(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\}$ and $l_{\cal E} (e^{\mbox{\scriptsize o}}) = b$.\\[.5em]
$compl(\tilde X') = \left\{ \begin{array}{ll}compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\} & \mbox{if }
\{e^*\} \mbox{ is a complete configuration of } \reff (b) \\ compl(\tilde X) &
\mbox{otherwise} \end{array} \right.$\\[.5em]
Thus $compl(\tilde X') \subseteq compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\} \subseteq pr(\tilde X)
\cup \{e^{\mbox{\scriptsize o}}\} = pr(\tilde X')$. \\
With lemma \ref{1} it follows that $ compl(\tilde X)
\cup \{e^{\mbox{\scriptsize o}}\} \in \conf ({\cal E})$.\\
Hence $ compl(\tilde X)~\buildrel b \over \longrightarrow~
compl(\tilde X)~\cup~\{e^{\mbox{\scriptsize o}}\}$.\\
Since $ (compl(\tilde X), compl(\tilde Y)) \in R$, there is a
$d^{\mbox{\scriptsize o}} \in E_{\cal F}$ with $ compl(\tilde Y) \buildrel {b} \over \longrightarrow 
compl(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\}$, $l_{\cal F} (d^{\mbox{\scriptsize o}}) = b$ and $(compl(\tilde X) \cup
\{e^{\mbox{\scriptsize o}}\}, compl(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\}) \in R$.

We now extend the bijection $f$ by $(e^{\mbox{\scriptsize o}},d^{\mbox{\scriptsize o}})$.\\
For this we verify that $d^{\mbox{\scriptsize o}}$ is not in the range of $f$:\\
Suppose $d^{\mbox{\scriptsize o}} \in pr(\tilde Y)$.
Since $d^{\mbox{\scriptsize o}} \not\in compl(\tilde Y)$, $f^{-1}(d^{\mbox{\scriptsize o}}) \in pr(\tilde X) - compl(\tilde X)$.
Thus $compl(\tilde X) \cup \{f^{-1}(d^{\mbox{\scriptsize o}})\} \in \conf ({\cal E})$
with lemma \ref{1} and $compl(\tilde X) \buildrel b \over \longrightarrow~compl(\tilde
X) \cup \{f^{-1}(d^{\mbox{\scriptsize o}})\}$.\\
Hence $b \not\in Crit_{\cal E}$ with lemma \ref{3} and then $e^{\mbox{\scriptsize o}} =
f^{-1}(d^{\mbox{\scriptsize o}})$ with lemma \ref{2}. \\ Thus $e^{\mbox{\scriptsize o}} \in pr(\tilde X) $ which contradicts
$pr(\tilde X') \neq pr(\tilde X)$.
So $d^{\mbox{\scriptsize o}} \not\in pr(\tilde Y)$.

\vskip 0.5cm
Now we can define $\tilde Y',f'$ and $\tilde f'$.\\
Let $f' := f \cup (e^{\mbox{\scriptsize o}},d^{\mbox{\scriptsize o}})$ and
$ \tilde Y' := \{(f'(e),e') \mid (e,e') \in \tilde X'\} = \tilde Y \cup \{(d^{\mbox{\scriptsize o}},e^*)\}$.


Using proposition \ref{compositionality} we proof
$\tilde Y' \in \conf (\reff ({\cal F}))$:
\begin{itemize} \vspace{-.7em}
\item [$-$] $pr(\tilde Y') = pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\} \in \conf
({\cal F})$ with lemma \ref{4};
\item [$-$] $\forall d \in  pr(\tilde Y') $:
$  Y_d' =  X_{{f'}^{-1}(d)}' \in \conf (\reff (l_{\cal E}({f'}^{-1}(d)))) -
\{\emptyset \} = \conf (\reff (l_{\cal F}(d))) - \{\emptyset \}$;
\item [$-$] $busy(\tilde Y') = pr(\tilde Y') - compl(\tilde Y') =
pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\} - compl(\tilde Y') \subseteq \\
pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\} - compl(\tilde Y) $, since
$compl(\tilde Y) \subseteq compl(\tilde Y')$. \\
It remains to show that $pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\} - compl(\tilde Y) \subseteq
max(pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\})$.\\
By proposition \ref{enabling}(iii) $pr(\tilde Y)$ is a prefix of $pr(\tilde Y) \cup
\{d^{\mbox{\scriptsize o}}\}$, so $d^{\mbox{\scriptsize o}} \in max(pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\})$.\\
Now suppose $d \in pr(\tilde Y) - compl(\tilde Y)$, but $d \not\in max(pr(\tilde Y)
\cup \{d^{\mbox{\scriptsize o}}\})$.\\
Then $d \in max(pr(\tilde Y))$ by proposition \ref{compositionality}, so $d <_{pr(\tilde
Y) \cup \{d^{\mbox{\tiny o}}\}} d^{\mbox{\scriptsize o}}$.
Since $compl(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\}$ is a prefix of $pr(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\}$ by
proposition \ref{enabling}(iii), we have $d \in compl(\tilde Y)$, which yields a
contradiction. 
\end{itemize} \vspace{-.7em}
Thus $ \tilde Y'$ is a configuration of $ \reff ({\cal F})$
and with $l_{\reff ({\cal F})} (d^{\mbox{\scriptsize o}},e^*) = a$ we have
$ \tilde Y~\buildrel a \over \longrightarrow~\tilde Y' $.

The new function $ f'$ is bijective, as shown above.
The same for $ \tilde f' \hspace{-.82348pt} := \hspace{-.9pt} \tilde f \cup
\{((e^{\mbox{\scriptsize o}},e^*),(d^{\mbox{\scriptsize o}},d^*))\}$. By construction
$f'$ and $\tilde f'$ have the required properties.

Now we show $ (\tilde X',\tilde Y') \in  \tilde R $ by proving
$(compl(\tilde X'),compl(\tilde Y')) \in R $. \\
There are again two cases:
\begin{description}
\item [2.1. $compl(\tilde X') = compl(\tilde X)$.] {\ }\\
By construction of $\tilde Y'$ (as in part 1.1 of the proof)
$ compl(\tilde Y') = compl(\tilde Y) $ and hence
$ (compl(\tilde X'), compl(\tilde Y')) \in R$.


\item [2.2. $compl(\tilde X') \neq compl(\tilde X)$.] {\ }\\
Then $ compl(\tilde X') = compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\} $
and by construction of $\tilde Y'$,
$compl(\tilde Y') =\linebreak compl(\tilde Y) \cup \{d^{\mbox{\scriptsize o}}\}$.
We had already that $(compl(\tilde X) \cup \{e^{\mbox{\scriptsize o}}\}, compl(\tilde Y)) \cup
\{d^{\mbox{\scriptsize o}}\}) \in R$, hence $(compl(\tilde X'), compl(\tilde Y')) \in R$.
\end{description}
Thus $ \tilde R$ is a bisimulation between $ \reff ({\cal E}) $ and $ \reff
({\cal F})$. \qed

\section*{Conclusion}

We have investigated here how two well-established interleaving equivalences behave
with respect to a restricted notion of action refinement. We have considered a class of
refinements where events deciding choices are considered atomic. It turned out that
interleaving trace semantics --- neglecting the branching structure --- is then still
not preserved under refinements whereas interleaving bisimulation yields the desired
preservation result.

It remains to be investigated what happens for other interleaving equivalences in
the linear time -- branching time spectrum, e.g. for failure semantics. Another
interesting question is what happens for step semantics (where several actions
happening simultaneously are considered). The example $a(bc|d)$ versus
$ab(c|d)+a(b|d)c$ with $\reff (d)=d_1 d_2$ may be used to show that {\it step trace
equivalence} is not preserved under safe refinements as considered here. For {\it step
bisimulation equivalence} we conjecture that we do have preservation under safe
refinements.

\vskip .35cm
{\bf Acknowledgements} \\ The idea to investigate refinements with atomic choice was
suggested by Manfred Broy. Three anonymous referees helped with their comments to improve the paper.

\section*{References}

\begin{description}
\item [{[Aceto]}]
L. Aceto: {\it Action Refinement in Process Algebras}, PhD-Thesis,
University of Sussex, 1990, Report No. 3/91, University of Sussex,
Computer Science, February 1991

\item [{[AH]}]
L. Aceto, M. Hennessy: {\it Adding Action Refinement to a Finite Process
Algebra}, Report No. 6/90, University of Sussex, Computer Science,
November 1990, extended abstract in: Proc. ICALP 91, LNCS 510,
Springer-Verlag, pp 506--519, 1991

\item [{[BDKP]}]
E. Best, R. Devillers, A. Kiehn, L. Pomello: {\it Concurrent Bisimulation in Petri
Nets}, Acta Informatica, Vol. 28, pp 231--264, 1991

\item [{[Boudol]}]
G. Boudol: {\it Flow Event Structures and Flow Nets}, 
in I. Guessarian (ed.): Semantics of Systems of Concurrent Processes,
LNCS 469, Springer-Verlag, pp 62--95, 1990

\item [{[BC]}]
G. Boudol, I. Castellani: {\it Permutation of Transitions: An Event
Structure Semantics for CCS and SCCS}, in J.W. de Bakker, W.-P. de Roever \& G.
Rozenberg (eds.): Linear Time, Branching Time and Partial Order in
Logics and Models for Concurrency, LNCS 354, Springer-Verlag, pp 411--427, 1989

\item [{[BGV]}]
W. Brauer, R. Gold, W. Vogler: {\it A Survey of Behaviour and Equivalence Preserving
Refinements of Petri Nets}, in: Advances in Petri Nets 1990, LNCS 483,
Springer-Verlag, pp 1--46, 1990

\item [{[DD a]}]
Ph. Darondeau, P. Degano: {\it Event structures, Causal trees, and
Refinements}, in: Proc. MFCS 90, LNCS 452, Springer-Verlag,
pp 239--245, 1990

\item [{[DD b]}]
Ph. Darondeau, P. Degano: {\it Refinement of Actions in Event Structures
and Causal Trees}, manuscript, 1991

\item [{[Devillers]}]
R. Devillers: {\it Maximality Preserving Bisimulation}, Technical Report
LIT-1214, Universit\'{e} Libre de Bruxelles, March 1990, to appear in TCS

\item [{[GG a]}]
R.J. van Glabbeek, U. Goltz: {\it Refinement of Actions in Causality
Based Models}, in J.W. de Bakker, W.-P. de Roever \& G.
Rozenberg (eds.): Stepwise Refinement of Distributed Systems: Models,
Formalism, Correctness, LNCS 430, Springer-Verlag, pp 267--300, 1990

\item [{[GG b]}]
R.J. van Glabbeek, U. Goltz: {\it Equivalences and Refinement},
% SFB-Bericht Nr. 342/12/90 A, TUM-19024, Technische Universit\"at
% M\"unchen, July 1990,
in: I. Guessarian (ed.): Semantics of Systems of Concurrent Processes,
LNCS 469, Springer-Verlag, pp 309--333, 1990

\item [{[GG c]}]
R.J. van Glabbeek, U. Goltz: {\it A Deadlock-sensitive Congruence for Action
Refinement}, SFB-Bericht Nr. 342/23/90 A, TUM-19044, Technische Universit\"at
M\"unchen, November 1990

\item [{[Milner]}]
R. Milner: {\it A Calculus of Communicating Systems}, LNCS 92, Springer-Verlag, 1980

\item [{[NEL]}]
M. Nielsen, U. Engberg, K. S. Larsen: {\it Fully Abstract Models for a Process Language
with Refinement}, in J.W. de Bakker, W.-P. de Roever \& G.
Rozenberg (eds.): Linear Time, Branching Time and Partial Order in
Logics and Models for Concurrency, LNCS 354,
Springer-Verlag, pp 523--548, 1989 

\item [{[NPW]}]
M. Nielsen, G.D. Plotkin, G. Winskel: {\it Petri Nets, Event Structures
and Domains, Part I}, Theoretical Computer Science, Vol. 13, No. 1,
pp 85--108, 1981

\item [{[Park]}]
D. Park: {\it Concurrency and Automata on Infinite Sequences}, in P. Deussen (ed.): Proc.
5th GI-Conference on Theoretical Computer Science, LNCS 104, Springer-Verlag, pp
167--183, 1981

\item [{[Vogler a]}]
W. Vogler: {\it Failures Semantics Based on Interval Semiwords is a Congruence for
Refinement}, Distributed Computing, Vol. 4, pp 139--162, 1991

\item [{[Vogler b]}]
W. Vogler: {\it Bisimulation and Action Refinement}, in: Proc. STACS 91, LNCS 480,
Springer-Verlag, pp 309--321, 1991

\end{description}
\end{document}
